Require Import AutoSep.
Require Import vstte1_header.
Require Import WordLemmas.

Set Printing Coercions.

Lemma natToWord_wordToNat_idempotent : forall w : W, natToW (wordToNat w) = w.
  intros; rewrite <- natToWord_wordToNat.
  auto.
Qed.

Hint Rewrite natToWord_wordToNat_idempotent : N.

Lemma nth_sel : forall n ls default, (goodSize n -> n < length ls -> nth n ls default = Array.sel ls (natToW n))%nat.
  intros.
  rewrite sel_selN.
  Focus 2.
  apply goodSize_danger.
  auto.
  generalize H0.
  generalize ls.
  clear H H0 ls.
  induction n; destruct ls; simpl in *; try omega; intuition.
Qed.

Lemma nth_wordToNat_sel : forall (w : W) ls, (wordToNat w < length ls -> nth (wordToNat w) ls (natToW 0) = Array.sel ls w)%nat.
  intros.
  rewrite nth_sel; auto.
  autorewrite with N; auto.
Qed.

Lemma wordToNat_inj : forall a b : W, wordToNat a = wordToNat b -> a = b.
  intros.
  replace a with (natToW (wordToNat a)) by (autorewrite with N; auto).
  replace b with (natToW (wordToNat b)) by (autorewrite with N; auto).
  auto.
Qed.

Lemma wle_wle_antisym : forall n m:W, n <= m -> m <= n -> n = m.
  intros.
  pre_nomega.
  assert (wordToNat m = wordToNat n).
  omega.
  SearchAbout wordToNat eq.
  apply wordToNat_inj.
  auto.
Qed.

Hint Resolve wle_wle_antisym.

Lemma wordToNat_wplus_dis : forall a b : W, goodSize (wordToNat a + wordToNat b) -> wordToNat (a ^+ b) = wordToNat a + wordToNat b.
  SearchAbout wplus plus wordToNat.
  Check wordToNat_wplus.
  intros.
  replace a with (natToW (wordToNat a)) by (autorewrite with N; auto).
  replace b with (natToW (wordToNat b)) by (autorewrite with N; auto).
  rewrite wordToNat_wplus.
  autorewrite with N; auto.
  apply goodSize_danger; auto.
Qed.

Hint Rewrite roundTrip_0 : N.
Hint Rewrite roundTrip_1 : N.

Lemma wordToNat_minus : forall u : W,
                          $0 < u
                          -> wordToNat (u ^- $1) = wordToNat u - 1.
  intros.
  rewrite wordToNat_wminus.
  autorewrite with N; auto.
  nomega.
Qed.

Hint Rewrite wordToNat_minus using nomega : myN.

Lemma natToWord_minus1_dis : forall n : nat,
                       (0 < n)%nat -> natToW (n - 1) = natToW n ^- natToW 1.
  intros.
  rewrite natToW_minus; auto.
Qed.

Hint Rewrite natToWord_minus1_dis using nomega : myN.

Lemma wlt_wordToNat_lt : forall a b : W, a < b -> (wordToNat a < wordToNat b)%nat.
  intros.
  nomega.
Qed.

Lemma wordToNat_wplus_one_W : forall n m:W, n < m ->
                              wordToNat (n ^+ natToW 1) = S (wordToNat n).
  intros.
  replace n with (natToW (wordToNat n)) by (autorewrite with N; auto).
  rewrite wordToNat_wplus.
  autorewrite with N.
  omega.
  assert ((wordToNat m) < pow2 32)%nat.
  apply goodSize_danger; auto.
  apply wlt_wordToNat_lt in H.
  omega.
Qed.

Set Implicit Arguments.

(* lemmas about pure Coq constructs *)
Lemma length0_nil : forall A (ls : list A),
  length ls = 0
  -> ls = nil.
  destruct ls; simpl; intuition.
Qed.
Lemma firstn0 : forall(A : Type)(ls : list A), firstn 0 ls = nil.
  destruct ls; auto.
Qed.
Lemma skipn0 : forall(A : Type)(ls : list A), skipn 0 ls = ls.
  intros.
  simpl.
  reflexivity.
Qed.
Lemma firstn_whole : forall(A : Type)(ls : list A), firstn (length ls) ls = ls.
  intros.
  induction ls; auto.
  simpl.
  f_equal.
  assumption.
Qed.
Lemma skipn_whole : forall(A : Type)(ls : list A), skipn (length ls) ls = nil.
  intros.
  induction ls; auto.
Qed.
Lemma firstn_length_whole : forall A (ls:list A), firstn (length ls) ls = ls.
  induction ls; simpl; auto; congruence.
Qed.
Lemma skipn_length_nil : forall A (ls:list A), skipn (length ls) ls = nil.
  induction ls; simpl; auto.
Qed.
Lemma tl_skipn : forall n (A : Type) (ls : list A), (n < length ls)%nat -> tl (skipn n ls) = skipn (n+1) ls.
  induction n; destruct ls; simpl; intuition.
Qed.
Lemma firstn_right : forall n (A : Type) (ls : list A) default, (n < length ls)%nat -> firstn (n+1) ls = firstn n ls ++ nth n ls default::nil.
  induction n; destruct ls; simpl in *; intuition; f_equal; intuition.
Qed.
Lemma firstn_right_W : forall n (ls : list W), (n < length ls)%nat -> firstn (n+1) ls = firstn n ls ++ nth n ls (natToW 0)::nil.
  intros.
  apply firstn_right; auto.
Qed.
Lemma allbool_cons : forall a ls, allbool (a::ls) -> allbool ls.
  inversion 1; simpl; intuition.
Qed.
Hint Resolve allbool_cons.
Lemma allbool_skipn : forall n ls, allbool ls -> allbool (skipn n ls).
  induction n; destruct ls; simpl in *; intuition; f_equal; intuition.
  eauto.
Qed.
Lemma firstn_nil : forall n A, firstn n nil = nil (A := A).
  induction n; simpl; intuition.
Qed.
Hint Rewrite firstn_nil : list.
Lemma firstn_cons : forall A n a (ls : list A), a::firstn n ls = firstn (n + 1) (a::ls).
  induction n; destruct ls; simpl; intuition; f_equal; intuition.
  autorewrite with list.
  auto.
Qed.
Lemma allbool_firstn : forall n ls, allbool ls -> allbool (firstn n ls).
  induction n; destruct ls; simpl; intuition.
  compute; intuition.
  inversion H; simpl; intuition; constructor 2; intuition; fold allbool; auto.
Qed.
Hint Resolve Lt.lt_S_n.
Lemma skipn_not_nil : forall n  (A : Type) (ls : list A), (n < length ls)%nat -> skipn n ls <> nil.
  induction n; destruct ls; simpl in *; intuition; f_equal; intuition.
  eauto.
Qed.
Lemma hd_skipn : forall n (A : Type) (ls : list A) default, (n < length ls)%nat -> hd default (skipn n ls) = nth n ls default.
  induction n; destruct ls; simpl in *; intuition; f_equal; intuition.
Qed.
Definition hd_skipn_W n ls := hd_skipn(A:=W)(n:=n) ls (natToW 0).
Lemma nth_firstn : forall m n (A : Type) (ls : list A) default, (m < n -> n <= length ls -> nth m (firstn n ls) default = nth m ls default)%nat.
  induction m; destruct ls; simpl; intuition; induction n; simpl; intuition.
Qed.
Definition nth_firstn_W m n ls := nth_firstn(A:=W)(m:=m)(n:=n) ls (natToW 0).
Lemma sort_bool_0_cons : forall ls, sort_bool ((natToW 0)::ls) = natToW 0::sort_bool ls.
  unfold sort_bool; simpl; intuition.
Qed.
Hint Rewrite sort_bool_0_cons : list.
Lemma sort_bool_hd_0 : forall ls, allbool ls -> ls <> nil -> hd (natToW 0) ls = natToW 0 -> sort_bool ls = (natToW 0)::sort_bool (tl ls).
  destruct ls; simpl; intuition; subst; auto.
Qed.
Lemma sort_bool_app_1 : forall ls, sort_bool (ls ++ (natToW 1)::nil) = sort_bool ls ++ (natToW 1)::nil.
  induction ls; simpl; intuition.
  Lemma filter_false_cons : forall A a (ls : list A) f, f a = false -> filter f (a :: ls) = filter f ls.
    intros.
    simpl.
    rewrite H.
    auto.
  Qed.
  Lemma filter_true_cons : forall A a (ls : list A) f, f a = true -> filter f (a :: ls) = a :: filter f ls.
    intros.
    simpl.
    rewrite H.
    auto.
  Qed.
  destruct (weq a (natToW 0)).
  rewrite e.
  repeat rewrite sort_bool_0_cons.
  rewrite IHls.
  intuition.
  destruct (weq a (natToW 1)).
  rewrite e.
  Lemma sort_bool_0_cons1 : forall ls, sort_bool ((natToW 1) :: ls) = (sort_bool ls) ++ (natToW 1)::nil.
    intros.
    unfold sort_bool.
    simpl.
    change (weqb (natToW 0) (natToW 1)) with false.
    change (weqb (natToW 1) (natToW 1)) with true.
    simpl.
    Lemma filter_eq_app_comm : forall a ls, a :: filter_eq a ls = filter_eq a ls ++ a :: nil.
      induction ls; simpl; intuition.
      destruct (weq a0 a).
      rewrite e.
      replace (weqb a a) with true.
      rewrite <- app_comm_cons.
      rewrite <- IHls.
      auto.
      Lemma weqb_sufficient : forall x y : W, x = y -> Word.weqb x y = true.
        Hint Resolve weqb_true_iff.
        Lemma iff_elim_l : forall P Q, (P <-> Q) -> (Q -> P).
          firstorder.
        Qed.
        intros x y.
        apply iff_elim_l.
        apply weqb_true_iff.
      Qed.
      rewrite weqb_sufficient.
      auto.
      auto.
      Lemma weqb_sound' : forall x y : W, x <> y -> Word.weqb x y = false.
        intros.
        destruct (Bool.bool_dec (Word.weqb x y) true).
        apply weqb_sound in e.
        contradiction.
        destruct (Word.weqb x y); intuition.
      Qed.
      Lemma neq_refl : forall A (a b : A), a <> b -> b <> a.
        intuition.
      Qed.
      apply neq_refl in n.
      apply weqb_sound' in n.
      unfold weqb.
      rewrite n.
      auto.
    Qed.
    rewrite filter_eq_app_comm.
    intuition.
  Qed.
  Check sort_bool_0_cons1.
  repeat rewrite sort_bool_0_cons1.
  rewrite IHls.
  intuition.
  Lemma sort_bool_0_cons_not01 : forall a ls, a <> natToW 0 -> a <> natToW 1 -> sort_bool (a :: ls) = sort_bool ls.
    intros.
    unfold sort_bool.
    unfold filter_eq.
    apply neq_refl in H.
    apply neq_refl in H0.
    apply weqb_sound' in H.
    apply weqb_sound' in H0.
    simpl.
    unfold weqb.
    rewrite H.
    rewrite H0.
    intuition.
  Qed.
  repeat rewrite sort_bool_0_cons_not01; auto.
Qed.
Hint Rewrite sort_bool_app_1 : list.
Lemma sort_bool_last_1 : forall ls, allbool ls -> ls <> nil -> List.last ls (natToW 0) = natToW 1 -> sort_bool ls = sort_bool (removelast ls) ++ natToW 1::nil.
  destruct ls; intuition; subst; auto.
  Lemma removelast_cons : forall A a1 a2 (ls : list A), removelast (a1 :: a2 :: ls) = a1 :: removelast (a2 :: ls).
    destruct ls; simpl; intuition.
  Qed.
  Lemma removelast_app_last : forall A default (ls : list A), ls <> nil -> ls = removelast ls ++ List.last ls default :: nil.
    induction ls; intuition.
    induction ls; intuition.
    rewrite removelast_cons.
    Lemma last_cons : forall A default a1 a2 (ls : list A), List.last (a1 :: a2 :: ls) default = List.last (a2 :: ls) default.
      intuition.
    Qed.
    rewrite last_cons.
    rewrite <- app_comm_cons.
    intuition.
  Qed.
  About removelast_app_last.
  rewrite (removelast_app_last (ls := w :: ls) (natToW 0)) at 1; intuition.
  rewrite H1.
  autorewrite with list.
  eauto.
Qed.  
Definition range (i j : nat) (A : Type) (ls : list A) := skipn i (firstn j ls).
Lemma removelast_range : forall (i j : nat) (A : Type)(ls : list A), (i < j -> j <= length ls -> removelast (range i j ls) = range i (j - 1) ls)%nat.
  unfold range.
  Lemma removelast_skipn : forall n A (ls : list A), (n < length ls)%nat -> removelast (skipn n ls) = skipn n (removelast ls).
    induction n; induction ls; intuition.
    simpl.
    induction n; induction ls; intuition.
  Qed.
  intros.
  rewrite removelast_skipn; intuition.
  Lemma removelast_firstn : forall n A (ls : list A), (0 < n -> n <= length ls -> removelast (firstn n ls) = firstn (n - 1) ls)%nat.
    induction n; destruct ls; intuition.
    simpl.
    autorewrite with list.
    auto.
    destruct (destruct_list (firstn n ls)).
    inversion s.
    inversion X.
    simpl.
    rewrite H1.
    rewrite <- H1.
    rewrite IHn.
    intuition.
    replace (n - 0) with n by omega.
    replace n with (n - 1 + 1).
    replace (n-1+1-1) with (n-1) by omega.
    Lemma plus1_S : forall n, n + 1 = S n.
      intros.
      rewrite Plus.plus_comm.
      simpl.
      auto.
    Qed.
    rewrite plus1_S.
    simpl.
    auto.
    induction n; simpl in *; intuition.
    induction n; simpl in *; intuition.    
    simpl in H0.
    omega.
    simpl.
    rewrite e.
    induction n; destruct ls; simpl in *; intuition.
  Qed.
  Lemma nil_length0 : forall A (ls : list A), ls = nil -> length ls = 0.
    destruct ls; intuition.
  Qed.
  rewrite removelast_firstn; try omega.
  auto.
  rewrite firstn_length.
  rewrite min_l; try omega.
Qed.
Lemma skipn_left : forall (A : Type) default (ls : list A) n, (0 < n -> n <= length ls -> skipn (n - 1) ls = nth (n - 1) ls default::skipn n ls)%nat.
  Lemma skipn_left' : forall A n default (ls : list A), (0 <= n -> n < length ls -> skipn n ls = nth n ls default :: skipn (S n) ls)%nat.
    induction n; destruct ls; simpl; intuition.
    destruct ls; intuition.
    induction n; simpl in *; intuition.
    rewrite (IHn default (a0 :: ls)); try omega.
    simpl; intuition.
  Qed.
  intros.
  rewrite (skipn_left' (n := n - 1) default) by try omega.
  replace n with (S (n - 1)) by omega.
  replace (S (n - 1) - 1) with (n - 1) by omega.
  intuition.
Qed.
Definition skipn_left_W := skipn_left (A := W) (natToW 0).
Lemma skipn_firstn_nil : forall n (A : Type) (ls : list A), skipn n (firstn n ls) = nil.
  induction n; destruct ls; simpl; intuition.
Qed.
Lemma firstn_skipn_whole : forall n A (ls : list A), firstn n ls ++ skipn n ls = ls.
  induction n; destruct ls; simpl; intuition.
Qed.

Lemma nil_length : forall A (ls : list A),
  length ls = 0
  -> ls = nil.
  destruct ls; simpl; intuition.
Qed.

Set Printing Coercions.

Hint Resolve nil_length natToW_inj.
Hint Extern 1 (@eq W _ _) => congruence.

Theorem wordToNat_inj' : forall sz (x y:word sz), x <> y ->
                                                      wordToNat x <> wordToNat y.
  intros.
  intro.
  apply H.
  apply (f_equal (natToWord sz)) in H0.
  rewrite 2!natToWord_wordToNat in H0.
  assumption.
Qed.
 
Theorem wordToNat_natToWord_idempotent_W : forall n,
                                             goodSize n
                                             -> wordToNat (natToWord 32 n) = n.
  intros; apply wordToNat_natToWord_idempotent; auto.
Qed.

Hint Rewrite wordToNat_natToWord_idempotent_W using solve [ eauto ] : N.

Lemma i_j_differ : forall (ls:list W)(i j:W), i < j ->
                                              Array.sel ls i <> $0 ->
                                              Array.sel ls (j ^- $1) = $0 ->
                                              i ^+ $1 < j.
  intros.
  assert (i <> j ^- $1) by congruence.
  pre_nomega.
  apply wordToNat_inj' in H2.
  pre_nomega.
  rewrite wordToNat_minus in H2.
  erewrite wordToNat_wplus_one_W.
  omega.
  instantiate (1:=j).
  nomega.
  nomega.
Qed.

Hint Resolve i_j_differ.


Ltac unugly0 f := fold (f W).
Ltac unugly := unugly0 skipn; unugly0 firstn.
(*
Lemma firstn0 : forall(A : Type)(ls : list A), firstn 0 ls = nil.
  destruct ls; auto.
Qed.

Lemma skipn_whole : forall(A : Type)(ls : list A), skipn (length ls) ls = nil.
  induction ls; auto.
Qed.

Lemma skipn0 : forall(A : Type)(ls : list A), skipn 0 ls = ls.
  auto.
Qed.

Lemma firstn_whole : forall(A : Type)(ls : list A), firstn (length ls) ls = ls.
  induction ls; simpl; intuition.
Qed.
*)
Hint Rewrite app_nil_l
     firstn0 skipn0 firstn_whole skipn_whole firstn_skipn
     roundTrip_0 : list.

Lemma plus1_wlt : forall u v, u < v -> u ^+ natToW 1 <= v.
  intros.
  pre_nomega.
  SearchAbout wplus wordToNat.
  erewrite wordToNat_wplus_one_W.
  auto.
  instantiate (1:= v).
  nomega.
Qed.

Hint Immediate plus1_wlt.

Ltac evaler := match goal with
                 | [ H : evalInstrs _ _ ( _ :: _ :: _ :: _) = _ |- _] =>
                   clear H; evaluate auto_ext
               end.

Ltac rewriter :=
  repeat match goal with
           | [ H : _ = _ |- _ ] => rewrite H
         end; autorewrite with list.

Opaque goodSize.

Lemma swap_length_eq : forall (ls:list W)(i j:W), (length (array_swap ls i j)) = length ls.
  unfold array_swap.
  intros.
  SearchAbout Array.upd length.
  rewrite 2!upd_length.
  auto.
Qed.
Hint Rewrite swap_length_eq : list.

Hint Resolve allbool_cons allbool_skipn allbool_firstn.

Hint Resolve containsArray_goodSize.
Hint Rewrite firstn_length : list.
Hint Rewrite min_l using nomega : list.
Hint Rewrite nth_firstn_W using nomega : list.

Lemma sort_left : forall n ls, (
  allbool ls -> 
  n < length ls -> 
  nth n ls (natToW 0) = (natToW 0) -> 
  firstn n ls ++ sort_bool (skipn n ls) = firstn (S n) ls ++ sort_bool (skipn (S n) ls))%nat. 
  induction n; destruct ls; intuition.
  simpl in *.
  rewrite H1.
  rewrite sort_bool_0_cons; eauto.
  simpl.
  f_equal.
  eauto.
Qed.
Lemma sort_left' : forall i j ls, (
  allbool ls ->
  i < j ->
  j <= length ls ->
  nth i ls (natToW 0) = (natToW 0) ->
  firstn i ls ++ sort_bool (skipn i (firstn j ls)) = firstn (S i) ls ++ sort_bool (skipn (S i) (firstn j ls)))%nat.
  Lemma firstn_absorb : forall A i j (ls : list A),
    (i <= j -> firstn i (firstn j ls) = firstn i ls)%nat.
    induction i; induction j; destruct ls; simpl; intuition.
    f_equal.
    intuition.
  Qed.
  intros.
  rewrite <- (firstn_absorb (i := i) (j := j)); intuition.
  rewrite <- (firstn_absorb (i := S i) (j := j)); intuition.
  rewrite sort_left; intuition; autorewrite with list; auto.
Qed.
Lemma sort_right : forall i j ls, (
  allbool ls ->
  i <= j ->
  j < length ls ->
  nth j ls (natToW 0) = (natToW 1) ->
  firstn i ls ++ sort_bool (skipn i (firstn (S j) ls)) ++ skipn (S j) ls =
    firstn i ls ++ sort_bool (skipn i (firstn j ls)) ++ skipn j ls)%nat.
  induction i; induction j; destruct ls; intuition.
  simpl; intuition.
  simpl in H2.
  rewrite H2.
  unfold sort_bool.
  simpl.
  Lemma weqb01 : weqb (natToW 0) (natToW 1) = false.
    change (weqb (natToW 0) (natToW 1)) with false; auto.
  Qed.
  Lemma weqb11 : weqb (natToW 1) (natToW 1) = true.
    change (weqb (natToW 1) (natToW 1)) with true; auto.
  Qed.
  Hint Rewrite weqb01 weqb11 : list.
  rewriter.
  intuition.
  rewrite sort_bool_last_1; intuition; eauto.
  rewrite skipn0.
  rewrite List.removelast_firstn.
  rewrite firstn0.
  f_equal.
  rewrite (skipn_left' (n := S j) (natToW 0)).
  simpl in H2.
  simpl.
  rewrite H2.
  repeat rewrite <- app_assoc.
  Lemma elem_app_cons : forall (A : Type) (a : A) (ls : list A), (a :: nil) ++ ls = a :: ls.
    intros.
    simpl.
    reflexivity.
  Qed.
  Hint Rewrite elem_app_cons : list.
  autorewrite with list.
  auto.
  omega.
  omega.
  omega.
  rewrite skipn0 in H3.
  simpl in H3.
  intuition.
  autorewrite with list.
  Lemma last_firstn : forall A n (ls : list A) default, (n < length ls -> List.last (firstn (S n) ls) default = nth n ls default)%nat.
    induction n; destruct ls; simpl; intuition.
    rewrite <- IHn.
    destruct ls; simpl in *; intuition.
    omega.
  Qed.
  rewrite last_firstn.
  auto.
  omega.
  simpl in *; intuition; f_equal; intuition.
  rewrite <- IHi.
  intuition.
  eauto.
  omega.
  omega.
  auto.
Qed.
Lemma sort_right_minus1 : forall i j ls, (
  allbool ls ->
  i < j ->
  j <= length ls ->
  nth (j - 1) ls (natToW 0) = (natToW 1) ->
  firstn i ls ++ sort_bool (skipn i (firstn j ls)) ++ skipn j ls =
    firstn i ls ++ sort_bool (skipn i (firstn (j - 1) ls)) ++ skipn (j - 1) ls)%nat.
  intros.
  replace j with (j - 1 + 1) by omega.
  replace (j - 1 + 1 - 1) with (j - 1) by omega.
  repeat rewrite plus1_S.
  rewrite sort_right; try omega; eauto.
Qed.
Lemma allbool_nonzero_one' : forall n ls, (allbool ls -> n < length ls -> nth n ls (natToW 0) <> natToW 0 -> nth n ls (natToW 0) = natToW 1)%nat.
  induction n; inversion 1; simpl; intuition.
Qed.
Hint Extern 1 => reflexivity.
Ltac tac_goodSize :=
  match goal with
    | [ H : le _ (length ?LS) |- context [goodSize _] ] => apply goodSize_weaken with (n := length LS); eauto; nomega
  end.
Hint Rewrite nth_sel using solve [tac_goodSize | nomega] : list.
Ltac tac_nth_eq_1 :=
  match goal with
    | [ H : ~(Array.sel _ _ = natToW 0) |- nth _ _ _ = natToW 1 ] =>
      apply allbool_nonzero_one'; autorewrite with list; autorewrite with N myN; eauto; nomega
  end.
Hint Rewrite <- sort_right_minus1 using eauto; solve [nomega | tac_nth_eq_1] : list.
Hint Rewrite <- sort_left' using try rewrite nth_wordToNat_sel; eauto; nomega : list.

Hint Rewrite wordToNat_wplus_dis using tac_goodSize : myN.
Ltac my_nomega := pre_nomega; autorewrite with myN; nomega.

Lemma Forall_nth : forall A n (ls : list A) P default, (List.Forall P ls -> n < length ls -> P (nth n ls default))%nat.
  induction n; inversion 1; simpl; intuition.
  apply IHn.
  eauto.
  omega.
Qed.
Lemma Forall_updN : forall n ls P x, (List.Forall P ls -> P x -> n < length ls -> List.Forall P (updN ls n x))%nat.
  induction n; inversion 1; simpl; intuition.
Qed.

Hint Rewrite updN_length : list.

Lemma allbool_swap' : forall i j ls default, (allbool ls -> i < length ls -> j < length ls -> allbool (updN (updN ls i (nth j ls default)) j (nth i ls default)))%nat.
  Ltac tac_Forall_nth_updN := constructor 2; repeat (apply Forall_updN; autorewrite with list; try omega); repeat (apply Forall_nth; autorewrite with list; try omega); autorewrite with list; eauto; try omega.
  induction i; induction j; inversion 1; simpl; intuition; tac_Forall_nth_updN.
Qed.

Lemma allbool_swap : forall i j ls, (allbool ls -> wordToNat i < length ls -> wordToNat j < length ls -> allbool (array_swap ls i j))%nat.
  unfold array_swap.
  intros i j ls.
  replace i with (natToW (wordToNat i)).
  Focus 2.
  autorewrite with N; auto.
  replace j with (natToW (wordToNat j)).
  Focus 2.
  autorewrite with N; auto.
  repeat rewrite upd_updN; try(apply goodSize_danger; eauto).
  intros.
  repeat rewrite <- (nth_sel _ _ (natToW 0)); autorewrite with N in *; auto.
  apply allbool_swap'; auto.
Qed.
Definition array_swapN ls i j default := updN (updN ls i (nth j ls default)) j (nth i ls default).
Lemma array_swap_array_swapN : forall i j ls, (wordToNat i < length ls -> wordToNat j < length ls -> array_swap ls i j = array_swapN ls (wordToNat i) (wordToNat j) (natToW 0))%nat.
  unfold array_swap.
  unfold array_swapN.
  intros.
  replace i with (natToW (wordToNat i)).
  Focus 2.
  autorewrite with N; auto.
  replace j with (natToW (wordToNat j)).
  Focus 2.
  autorewrite with N; auto.
  repeat rewrite upd_updN; try(apply goodSize_danger; eauto). 
  repeat rewrite <- (nth_sel _ _ (natToW 0)); autorewrite with N in *; auto.
Qed.
Definition sort_3part i j ls := firstn i ls ++ sort_bool (range i j ls) ++ skipn j ls.
Lemma sort_swap : forall i j ls default, (
  allbool ls ->
  S i < j ->
  j <= length ls ->
  nth i ls default = natToW 1 ->
  nth (j - 1) ls default = natToW 0 ->
  sort_3part (S i) (j - 1) (array_swapN ls i (j - 1) default) = sort_3part i j ls
)%nat.
  unfold sort_3part; unfold range; induction i; induction j; destruct ls; inversion 1; try solve [simpl; intuition].
  intuition.
  rewrite H8 in H6.
  simpl in H6.
  discriminate H6.
  replace (S j - 1) with j in * by omega.
  change (firstn (S j) (w :: ls)) with (w :: firstn j ls).
  Print Rewrite HintDb list.
  autorewrite with list.
  change (skipn (S j) (w :: ls)) with (skipn j ls).
  rewrite H8.
  Lemma nth_swap : forall i j ls default default2, (
    i < length ls ->
    j < length ls ->
    nth i (array_swapN ls i j default) default2 = nth j ls default2
    )%nat.
    induction i; induction j; destruct ls; simpl; intuition.
    Lemma nth_updN : forall n ls v default, (n < length ls -> nth n (updN ls n v) default = v)%nat.
      induction n; destruct ls; simpl; intuition.
    Qed.
    Lemma nth_diff_default : forall A n (ls : list A) def1 def2, (n < length ls -> nth n ls def1 = nth n ls def2)%nat.
      induction n; destruct ls; simpl; intuition.
    Qed.
    apply nth_diff_default; omega.
    apply nth_updN; omega.
    apply IHi; omega.
  Qed.
  Lemma firstn1_nth0 : forall A (ls : list A) default, (0 < length ls -> firstn 1 ls = nth 0 ls default :: nil)%nat.
    destruct ls; simpl; intuition.
  Qed.
  rewrite (firstn1_nth0 _ (natToW 0)).
  rewrite (nth_swap _ default (natToW 0)).
  rewrite H8 in H7.
  rewrite (nth_diff_default _ (natToW 0) default).
  rewrite H7.
  rewrite elem_app_cons.
  SearchAbout sort_bool 1 cons.
  rewrite sort_bool_0_cons1.
  SearchAbout skipn nth.
  rewrite (skipn_left' (n := j) default).
  Lemma array_swapW_refl : forall i j ls default, (i < length ls -> j < length ls -> array_swapN ls i j default = array_swapN ls j i default)%nat.
    induction i; induction j; destruct ls; unfold array_swapN; simpl; intuition.
    f_equal.
    eauto.
  Qed.
  About array_swapW_refl.
  rewrite (array_swapW_refl (i := 0) (j := j)).
  rewrite nth_swap.
  SearchAbout nth 0 cons.
  Lemma nth0_cons : forall A (ls : list A) a default, nth 0 (a :: ls) default = a.
    simpl; auto.
  Qed.
  rewrite nth0_cons.
  Lemma skipn_over_swap : forall n i j ls default, (i < n -> j < n -> n <= length ls -> skipn n (array_swapN ls i j default) = skipn n ls)%nat.
    Lemma skipn_over_updN : forall n i ls v, (i < n -> n <= length ls -> skipn n (updN ls i v) = skipn n ls)%nat.
      induction n; induction i; destruct ls; simpl; intuition.
    Qed.
    induction n; induction i; induction j; destruct ls; simpl; intuition;
      repeat rewrite skipn_over_updN by (try rewrite updN_length; eauto; omega); eauto.
  Qed.
  rewrite skipn_over_swap.
  Lemma skipn_simpl : forall A n (ls : list A) a, skipn (S n) (a :: ls) = skipn n ls.
    simpl; auto.
  Qed.
  rewrite skipn_simpl.
  destruct j; intuition.
  simpl in H7.
  SearchAbout firstn S nth.
  replace (S j) with (j + 1) by omega.
  rewrite (firstn_right ls default).
  rewrite plus1_S.
  rewrite H7.
  SearchAbout sort_bool app 0.
  Lemma sort_bool_right_0 : forall ls, allbool ls -> sort_bool (ls ++ natToW 0 :: nil) = (natToW 0) :: sort_bool ls.
    induction ls; inversion 1; simpl; intuition.
    rewrite H4.
    autorewrite with list.
    f_equal.
    auto.
    rewrite H4.
    SearchPattern (sort_bool (_::_) = _).
    repeat rewrite sort_bool_0_cons1.
    rewrite app_comm_cons.
    f_equal.
    auto.
  Qed.
  rewrite sort_bool_right_0.
  Lemma range_within_swap : forall m n i j ls default, (i < m -> m <= n -> n <= j -> j < length ls -> skipn m (firstn n (array_swapN ls i j default)) = skipn m (firstn n ls))%nat.
    induction m; induction n; induction i; induction j; destruct ls; simpl; intuition.
    Lemma firstn_before_updN : forall n j ls v, (n <= j -> j < length ls -> firstn n (updN ls j v) = firstn n ls)%nat.
      induction n; induction j; destruct ls; simpl; intuition.
      f_equal.
      auto.
    Qed.
    rewrite firstn_before_updN by omega; auto.
    rewrite firstn_before_updN by (try rewrite updN_length; eauto; omega); auto.
    Lemma firstn_updN_comm : forall n i ls v, (i < n -> n <= length ls -> firstn n (updN ls i v) = updN (firstn n ls) i v)%nat.
      induction n; induction i; destruct ls; simpl; intuition.
      f_equal.
      auto.
    Qed.
    rewrite firstn_updN_comm.
    rewrite skipn_over_updN.
    auto.
    omega.
    autorewrite with list.
    omega.
    omega.
    omega.
  Qed.
  rewrite array_swapW_refl.
  rewrite range_within_swap.
  repeat rewrite <- app_comm_cons.
  rewrite <- app_assoc.
  rewrite elem_app_cons.
  f_equal.
  f_equal.
  simpl; auto.
  omega.
  omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  auto.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  Lemma length_swap : forall i j ls default, (i < length ls -> j < length ls -> length (array_swapN ls i j default) = length ls)%nat.
    induction i; induction j; destruct ls; simpl; intuition.
    repeat rewrite updN_length by omega.
    auto.
  Qed.
  rewrite length_swap; simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  simpl in *; omega.
  rewrite length_swap; simpl in *; omega.

  Lemma firstn_simpl : forall A n (ls : list A) a, firstn (S n) (a :: ls) = a :: firstn n ls.
    simpl; auto.
  Qed.
  Lemma nth_simpl : forall A n (ls : list A) a default, nth (S n) (a :: ls) default = nth n ls default.
    simpl; auto.
  Qed.
  repeat rewrite firstn_simpl.
  repeat rewrite skipn_simpl.
  repeat rewrite nth_simpl.
  intros.
  simpl in H5.
  replace (S j - 1) with (S (j - 1)) in * by omega.
  Lemma swap_simpl : forall i j ls a default, (i < length ls -> j < length ls -> array_swapN (a :: ls) (S i) (S j) default = a :: array_swapN ls i j default)%nat.
    unfold array_swapN; simpl; auto.
  Qed.
  repeat rewrite swap_simpl.
  repeat rewrite firstn_simpl.
  repeat rewrite skipn_simpl.
  repeat rewrite <- app_comm_cons.
  f_equal.
  apply IHi; simpl in *; auto; try omega.
  omega.
  omega.
Qed.
Lemma range_fold : forall A i j (ls : list A), skipn i (firstn j ls) = range i j ls.
  auto.
Qed.
Lemma sort_3part_fold : forall i j ls, firstn i ls ++ sort_bool (range i j ls) ++ skipn j ls = sort_3part i j ls.
  auto.
Qed.
Lemma i_j_differ' : forall (ls:list W)(i j:W), i < j ->
                                            Array.sel ls i <> $0 ->
                                            Array.sel ls (j ^- $1) = $0 ->
                                            (S (wordToNat i) < wordToNat j)%nat.
  intros.
  rewrite <- plus1_S.
  change 1 with (wordToNat (natToW 1)).
  rewrite <- wordToNat_wplus_dis.
  apply wlt_wordToNat_lt.
  apply (i_j_differ ls); auto.
  About goodSize_weaken.
  apply (goodSize_weaken (wordToNat j)).
  auto.
  rewrite roundTrip_1.
  nomega.
Qed.
Ltac tac_clear := repeat match goal with 
  | [ H : context [interp] |- _ ] => clear H
  | [ H : context [star] |- _ ] => clear H
  | [ H : context [evalInstrs] |- _ ] => clear H
  | [ H : context [evalCond] |- _ ] => clear H
  | [ H : context [ok_call] |- _ ] => clear H
end.
Hint Rewrite <- sort_right_minus1 using eauto; solve [nomega | tac_nth_eq_1] : list.
Ltac tac_sort_swap_side := solve [
  eapply i_j_differ'; eauto; nomega |
  tac_nth_eq_1 |
  erewrite <- wordToNat_minus by nomega; rewrite nth_wordToNat_sel; auto; my_nomega].
Ltac tac_extract_goodSize := match goal with
  | [ H : context[length ?LS] |- _ ] => assert (goodSize (length LS)) by (eapply (containsArray_goodSize _ _ _ LS); eauto; auto 7)
end.
Hint Rewrite skipn_firstn_nil firstn_skipn_whole : list.
Hint Resolve wle_wle_antisym.
Ltac tac_sym := match goal with
  | [ H1 : ~(wlt ?N1 ?N2), H2 : ~(wlt ?N2 ?N1) |- _ ] => replace N2 with N1 by auto
end.
Ltac tac_list_sym := match goal with
  | [ H1 : ~(wlt ?N1 ?N2), H2 : ~(wlt ?N2 ?N1) |- context [sort_bool] ] => try tac_sym; autorewrite with list; auto
end.
Ltac tac_allbool_swap := tac_extract_goodSize; tac_clear; apply allbool_swap; eauto; my_nomega.
Ltac tac_sort_swap := match goal with
  | [ |- context[firstn _ (array_swap _ _ _)] ] =>                         
    tac_extract_goodSize;
    tac_clear;
    rewrite array_swap_array_swapN by my_nomega;
    repeat rewrite range_fold;
    repeat rewrite sort_3part_fold;
    autorewrite with N myN;
    repeat rewrite plus1_S;
    rewrite sort_swap;try tac_sort_swap_side; auto
end.
Hint Extern 10 (allbool (array_swap _ _ _)) => tac_allbool_swap : list.
Hint Extern 10 => tac_sort_swap : list.
Hint Extern 10 => tac_list_sym : list.
Ltac my2_nomega := pre_nomega; autorewrite with myN N in *; nomega.
Ltac tac_sort_left := match goal with
  | [ |- context [firstn (wordToNat (?W ^+ _)) _ ++ _ ++ _] ] => 
    autorewrite with N myN;
    repeat (rewrite plus1_S || rewrite app_assoc);
    autorewrite with list; eauto
end.
Hint Extern 10 => tac_sort_left : list.
Ltac tac_rewrite_list := match goal with
  | [ |- context [firstn (wordToNat (?W ^- _)) _] ] => 
    autorewrite with N myN; autorewrite with list; eauto
end.
Hint Extern 10 => tac_rewrite_list : list.
